Lambda the Ultimate

J. Grundy, T. Melham, and J. O'Leary, A reflective functional language for hardware design and theorem proving, Journal of Functional Programming, 16(2):157-196, March 2006.

This paper introduces reFLect, a functional programming language with reflection features intended for applications in hardware design and verification. The reFLect language is strongly typed and similar to ML, but has quotation and antiquotation constructs. These may be used to construct and decompose expressions in the reFLect language itself.

reFLect is apparently a follow-on to the earlier FL language (which I asked about in an earlier thread), the language used in Intel's Forte hardware verification environment. Within Forte, reFLect can be used to perform a seamless mix of theorem proving and model-checking (invocation of a model-checker is just a reFLect function call, with the source text of any call to the model-checker that returns true becoming a theorem of the logic). Tom Melham's reFLect page has a little more information, and also points out that a Linux version of the Forte system, including an implementation of reFLect, is freely downloadable from Intel.

As some feel that LtU is too math bound, there's only one solution for us underachievers - a Theoretical Computer Science Cheat Sheet.

(Most of it is vaguely familiar, as I've taken a lot of math courses over the years. Sadly though I'd need a much longer set of crib notes to jog my memory. Personally I think most CS based math is really simple, but it also is quite terse - much like many PLs.)

by James Cheney (beware, PDF takes up full screen)

Based on envious observations of the success of formal methods for verifying industrial hardware designs using model-checking, I will argue that "partial" techniques which provide full automation and search for counterexamples, but which do not try to verify correctness, are likely to be more useful [for "metatheory of logics and programming languages"] on a day-to-day basis activities than full verification. I will describe an unsophisticated, yet useful, implementation of such a "model-checking" approach to mechanized metatheory implemented using nominal logic programming (although the basic idea could be employed in many other settings).

Model checking meets POPLMark. I can't tell from this presentation if there's any chance of using tools similar to BLAST to search deeper or produce actual proofs.

A draft by Takeuti Izumi

This paper defines the theories of parametricity for the system lambda-P-omega in lambda cube, and shows some of its application. These theories are defined by the axiom sets in the formal theories. These theories prove various important semantical properties in the formal systems.

Parametricity is Wadler gets his theorems for free, nad Izumi gives an example of one of these free theorems for dependent sums in the Calculus of Constructions.

Recently the homepage is almost dead, and the discussions about important papers that are mentioned on the home page almost non-existent.

I am sad to say that if this continues LtU will fade away - something I am sure none of us wants.

This is a cry for help. If you are an editor, please try to post news you come across that might interest the LtU community. Take part in the discussions (you don't have to participate in all of them! participating in discussions on "static typing" is optional...) If you are an editor, are reading LtU, but haven't posted in a long time, don't feel you have become an outsider. You are still part of the team, and I for one am interested in what you might want to share. I know some long time editors got discouraged for various reasons -- I think now is a good time to return and reshape things to what they used to be.

If you are a regular reader and participate in the forum regularly, if you think you understand the spirit of LtU, how about signing up to become an editor? The process is simple (basically, you have to email me and that's it).

Many of you have personal blogs, and they are great resources. I still think the LtU community effort had an additional value it'd be a shame to lose. If you agree - post!

Finally, if you are a programming language scholar, and are reading and enjoying LtU - how about signing up to be a guest blogger?

I just noticed the existence of this O'Reilly book penned, so it seems, by Maurice Naftalin and (believe it or not) Philip Wadler! Is this for real, or a very elaborate hoax? It seems possible, if you remember the history of Java generics, so I guess it's true, but if someone actually saw a copy I'd be reassured...

The blurb, by the way, is from Gilad Bracha who says that this is a crystal-clear tutorial that starts with the basics and ends leaving the reader with a deep understanding of both the use and design of generics. Ya think?!

My only complaint about Martin (Fowler)'s talk is that he didn't mention Smalltalk and that he said that the Lisp people have been making DSLs for 20 years. I learned about them about 20 years ago, and the Lisp people had been doing it for 20 years before that, so I think they have been doing it for 40 years. Neverthless, DSLs are only starting to become a hot topic. OOPSLA has had a Domain Specific Modeling workshop for four or five years, and I'm hoping that next year it will grow into a symposium. These are ideas that need to become ubiquitous.

Ralph also mentions Intentional Software and points to Fowler's JAOO talk on Domain Specific Languages, a video of which is available online.

An interesting visual comparison of the grammars of Ruby, Java 1.5 and Javascript.

Anyone care to interpret the graphs?

from channel9.msdn.com:

Programming in the Age of Concurrency: Software Transactional Memory

Recently, we visited MSR Cambridge(UK) to meet some of the great minds working there. In this case, we were fortunate enough to get an hour's time with Simon Peyton-Jones and Tim Harris, who are researchers working on a very hard problem: making it easier (more predictable, more reliable, more composable) to write concurrent applications in this the age of Concurrency (multi-core is a reality, not a dream).

I've built a search engine dedicated to searching sites about programming languages (with an emphasis on theory) using the Google co-op services. You can find the search engine at: http://www.cdiggins.com/search/

Now you don't have to append your Google searches with extra superflous terms like "fish language" or "cat language" or "mixin types", you can just type in "fish", "cat" or "mixin".

There is still a fair amount of work to be done to fine-tune it, and increase the number of sites it searches. Let me know though if you can think of ways it can be improved.